\begin{tabbing}
$\forall$\=$D$:Dsys, ${\it sched}$:(Id$\rightarrow$(?($\mathbb{N}\rightarrow$(IdLnk + Id)))), $v$:($i$:Id$\rightarrow$M($i$).(timed)state),\+
\\[0ex]${\it dec}$:($i$,$a$:Id$\rightarrow\mathbb{N}\rightarrow$M($i$).state$\rightarrow$(?if $a$ $\in$ dom(M($i$).prob) then Outcome else Void fi )),
\\[0ex]${\it discrete}$:(Id$\rightarrow$Id$\rightarrow\mathbb{B}$), $l$:IdLnk, ${\it t'}$:$\mathbb{N}$.
\-\\[0ex]Feasible($D$) $\Rightarrow$ (queue($l$;${\it t'}$) = queue($l$;${\it t'}$) $\in$ (Msg($\lambda$$l$,${\it tg}$. M(source($l$)).dout2($l$;${\it tg}$)) List))
\end{tabbing}